Termination Proof Script

• Consider the SCC {38,52}. There are no usable rules. By taking the AF π with π(CONS) = π(mark) = 1 together with the lexicographic path order with empty precedence, rule 38 is weakly decreasing and rule 52 is strictly decreasing. There is one new SCC.
  • Consider the SCC {38}. By taking the AF π with π(CONS) = 1 together with the lexicographic path order with empty precedence, rule 38 is strictly decreasing.


• Consider the SCC {37,51}. There are no usable rules. By taking the AF π with π(FROM) = π(mark) = 1 together with the lexicographic path order with empty precedence, rule 37 is weakly decreasing and rule 51 is strictly decreasing. There is one new SCC.
  • Consider the SCC {37}. By taking the AF π with π(FROM) = 1 together with the lexicographic path order with empty precedence, rule 37 is strictly decreasing.


• Consider the SCC {54}. There are no usable rules. By taking the AF π with π(LENGTH) = 1 together with the lexicographic path order with empty precedence, rule 54 is strictly decreasing.


• Consider the SCC {55}. There are no usable rules. By taking the AF π with π(LENGTH1) = 1 together with the lexicographic path order with empty precedence, rule 55 is strictly decreasing.


• Consider the SCC {39,53}. There are no usable rules. By taking the AF π with π(mark) = π(S) = 1 together with the lexicographic path order with empty precedence, rule 39 is weakly decreasing and rule 53 is strictly decreasing. There is one new SCC.
  • Consider the SCC {39}. By taking the AF π with π(S) = 1 together with the lexicographic path order with empty precedence, rule 39 is strictly decreasing.


• Consider the SCC {41,43,44,46,48,50}. There are no usable rules. By taking the AF π with π(from) = π(length) = π(length1) = π(PROPER) = π(s) = 1 together with the lexicographic path order with empty precedence, the rules in {41,46,48,50} are weakly decreasing and the rules in {43,44} are strictly decreasing. There is one new SCC.
  • Consider the SCC {41,46,48,50}. By taking the AF π with π(from) = π(length) = π(length1) = π(PROPER) = 1 together with the lexicographic path order with empty precedence, the rules in {41,48,50} are weakly decreasing and rule 46 is strictly decreasing. There is one new SCC.
    • Consider the SCC {41,48,50}. By taking the AF π with π(from) = π(length) = π(PROPER) = 1 together with the lexicographic path order with empty precedence, the rules in {41,48} are weakly decreasing and rule 50 is strictly decreasing. There is one new SCC.
      • Consider the SCC {41,48}. By taking the AF π with π(from) = π(PROPER) = 1 together with the lexicographic path order with empty precedence, rule 41 is weakly decreasing and rule 48 is strictly decreasing. There is one new SCC.
        • Consider the SCC {41}. By taking the AF π with π(PROPER) = 1 together with the lexicographic path order with empty precedence, rule 41 is strictly decreasing.


• Consider the SCC {32,34,36}. There are no usable rules. By taking the AF π with π(ACTIVE) = π(cons) = π(from) = 1 together with the lexicographic path order with empty precedence, the rules in {32,34} are weakly decreasing and rule 36 is strictly decreasing. There is one new SCC.
  • Consider the SCC {32,34}. By taking the AF π with π(ACTIVE) = π(cons) = 1 together with the lexicographic path order with empty precedence, rule 34 is weakly decreasing and rule 32 is strictly decreasing. There is one new SCC.
    • Consider the SCC {34}. By taking the AF π with π(ACTIVE) = 1 and π(cons) = [1] together with the lexicographic path order with empty precedence, rule 34 is strictly decreasing.


• Consider the SCC {56,58}. The usable rules are {1-22}. The constraints could not be solved.